T:Type, L1, L2:(T List).
no_repeats(T;L1 @ L2)  {no_repeats(T;L1) & no_repeats(T;L2) & l_disjoint(T;L1;L2)} 

latex

Definitions	{T}, type List, x:AB(x), no_repeats(T;l), Type, , l_disjoint(T;l1;l2), x:A  B(x), P & Q, P  Q, x:A. B(x), s = t, t  T, [], False, P  Q, A, a < b, A  B, , ||as||, Void, {x:A| B(x)} , , #$n, l[i], |g|, S  T, A c B, P  Q, [car / cdr], (x  l), x. t(x), as @ bs, s ~ t, P  Q, left + right, x:A. B(x), hd(l), last(L)
Lemmas	l member subtype, member append, l disjoint singleton2, false wf, no repeats cons, all functionality wrt iff, iff functionality wrt iff, l member wf, and functionality wrt iff, l disjoint append2, no repeats nil, l disjoint nil, rev implies wf, length wf2, nat wf, not wf, select wf, l disjoint wf, guard wf, no repeats wf, iff wf